Let a solve be bounded, and say when Z3 could not decide - #96

Fixes #85.

Settles the third wrinkle of #57.

The defect

Z3Context built its native context from a fixed configuration and offered no way to add to it.
No timeout, no resource limit, no CancellationToken - and Check() ran synchronously on the
calling thread. A theorem Z3 cannot decide therefore ran until the process was killed:

using var ctx = new Z3Context();

ctx.NewTheorem<Symbols<int, int, int>>()
   .Where(t => (t.X1 * t.X1 * t.X1) + (t.X2 * t.X2 * t.X2) + (t.X3 * t.X3 * t.X3) == 42)
   .Solve();
// still running after 120 seconds when #85 was raised; killed

And because nothing could bound a solve, Status.UNKNOWN was unreachable, so Theorem.cs
reported it as unsatisfiable - the wrinkle #57 raised and #86 had to leave open.

Measured first, on the raw Microsoft.Z3 API

Before any library change, against the theorem above:

Two of those rows shaped the design. The reason strings are not consistent - the optimizer says
canceled for a timeout and an interrupt alike, and an exhausted rlimit is canceled on both

• so the library cannot tell cancellation from a limit by reading them. And an interrupt that
  arrives before the check starts does nothing, so an already-cancelled token has to be inspected
  rather than relied on to fire.

The change

Z3Context.Timeout and Z3Context.ResourceLimit, both nullable, both validated in the
setter, applied as parameters on each solver and optimizer rather than baked into the native
context - so they are properties of the Z3Context that can change between solves, and an
undecided solve leaves nothing behind. ResourceLimit is Z3's rlimit: deterministic, reached
at the same point on every machine, in units with no fixed relationship to time.

A CancellationToken on every entry point - Solve, TrySolve, Optimize, TryOptimize,
ISolveable<T>, the deferred orderby form, SolveOrNull and OptimizeOrNull - as an optional
parameter, CancellationToken cancellationToken = default. A cancelled token calls
Context.Interrupt(); the token is also inspected before the check, because of the lost-interrupt
row above. What remains is the moment between that inspection and Z3 starting work, which the
remarks say plainly.

How UNKNOWN is reported, the question #85 deferred to. Put to the maintainer with the
measurements above and chosen over a three-state result:

• a cancelled token throws OperationCanceledException, carrying the token, as everywhere in .NET;
• every other UNKNOWN - a timeout, an exhausted resource limit, or Z3 giving up on its own -
  throws a new TheoremUndecidedException, carrying Z3's reason string;
• TrySolve returning false now means one thing: the theorem was proved to have no solution.

Cancellation is recognised from the token rather than the string, because the strings cannot be
trusted to say which it was.

Public surface

Optional parameters on existing methods: source-compatible for every caller, binary-breaking for
the changed signatures. ISolveable<T> changes shape for the second time in this stack, which
2.0 allows and #86 already did. Z3Context gains two properties; the library gains one exception
type.

The README gets a When Z3 cannot decide section after When there is no solution, with the
theorem above as its example.

Tests

254 → 270, in a new SolveLimitTests.cs. Every test that runs the undecidable theorem carries a
[Timeout], so a regression fails the test rather than hanging the suite - and the whole suite
still finishes in under a second and a half, because the parallel runner overlaps the waits.

No test asserts on the reason string beyond its presence, for the reason in the table above, and
none asserts on elapsed time.

Mutation results

Chosen so that no mutation can hang the run: the limits themselves are proved by construction
(each limit test sets only the limit it is about), and the mutations target how an UNKNOWN is
reported.

Verification

• dotnet build solutions/Z3.Linq.slnx -c Release - clean, TreatWarningsAsErrors and
  documentation generation on; every new cref resolves
• 270/270 locally, 1.4 s
• ./build.ps1 -Configuration Release - 46 tasks, 0 errors, 0 warnings
• Coverage 88.3% -> 88.7% line (770 of 868), 77.9% -> 78.8% branch (517 of 656)

Release note

Releases remain on hold under #60 until Microsoft.Z3 5.x reaches nuget.org, so this reaches main
but not consumers. Nothing about the hold changes.